<html>
<head><meta charset="utf-8"><title>data-invariants · t-lang/wg-unsafe-code-guidelines · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/index.html">t-lang/wg-unsafe-code-guidelines</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html">data-invariants</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="131137092"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131137092" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131137092">(Aug 08 2018 at 22:46)</a>:</h4>
<p>At some point I want to jot down my thoughts on data invariants, starting with the basic invariants that layout optimizations rely on -- what are they, and when do they have to hold, etc. What would be the best place to submit that? one of our two UCG github repos, a blog post, or directly an RFC?</p>



<a name="131137471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131137471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131137471">(Aug 08 2018 at 22:57)</a>:</h4>
<p>what do you mean? I'd say, given an object of type <code>T</code>, that object should always hold a value of type <code>T</code>. That seems like the place you'd want to be.</p>



<a name="131137913"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131137913" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131137913">(Aug 08 2018 at 23:09)</a>:</h4>
<blockquote>
<p>At some point I want to jot down my thoughts on data invariants, starting with the basic invariants that layout optimizations rely on -- what are they, and when do they have to hold, etc. What would be the best place to submit that? one of our two UCG github repos, a blog post, or directly an RFC?</p>
</blockquote>
<p>I think it makes sense to write up something in <a href="https://github.com/rust-rfcs/unsafe-code-guidelines/" target="_blank" title="https://github.com/rust-rfcs/unsafe-code-guidelines/">https://github.com/rust-rfcs/unsafe-code-guidelines/</a></p>



<a name="131138270"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131138270" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131138270">(Aug 08 2018 at 23:19)</a>:</h4>
<p>If we're considering data layout invariants, one possible thing to think about is whether we offer guarantees when correct bit-patterns happen to be written</p>



<a name="131138360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131138360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131138360">(Aug 08 2018 at 23:21)</a>:</h4>
<p>e.g. is it okay to store a repr(rust) value on disk and read it back out to memory? do we offer guarantees that this works across identically defined types? across different compiler versions? can the compiler randomly reassign discriminants for enums every time the program runs?</p>



<a name="131139088"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131139088" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131139088">(Aug 08 2018 at 23:40)</a>:</h4>
<p>So this is a question of ABI - I'd argue that ABI should only be guaranteed (at the _most_) on exactly one compiler version and definition</p>



<a name="131139097"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131139097" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131139097">(Aug 08 2018 at 23:41)</a>:</h4>
<p>(We've broken ABI before)</p>



<a name="131155971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131155971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131155971">(Aug 09 2018 at 07:31)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> well that is an entirely cyclic definition. ;) You just said "the invariant to be maintained for <code>T</code> is the invariant for <code>T</code>".</p>



<a name="131156026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131156026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131156026">(Aug 09 2018 at 07:32)</a>:</h4>
<p><span class="user-mention" data-user-id="123893">@alercah</span> These are interesting questions but somewhat orthogonal. At this point, I am concerned with what the rules are once a particular data layout is fixed by the compiler.</p>



<a name="131156238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131156238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131156238">(Aug 09 2018 at 07:39)</a>:</h4>
<p>So, what I am imagining is something like:<br>
When it has to hold: The layout invariant must hold always; whenever you construct a value of type <code>T</code> (<code>transmute</code>, are there other operations we have to list) and whenever you <em>load</em> a value of type <code>T</code> (i.e., actually deref a place or use <code>ptr::read</code>).<br>
However, the invariant is pretty basic. It might be a good idea to adapt the principle that data layout invariants are the kind of invariant that, when it holds once for a value, it will always hold. That excludes making "<code>&amp;</code> is dereferencable" part of the invariant (because that could hold once, but then stop holding when memory gets deallocated), but would otherwise be nice for reasoning.<br>
So e.g. my proposal for the data layout invariant for <code>&amp;T</code> would be that it must be non-NULL and aligned. For <code>bool</code> it must be <code>0</code> or <code>1</code>, I think that is quite clear. Another interesting question is what about integer types: Is it okay to have <code>undef</code>/<code>poison</code> in an <code>i32</code>? For unions, I think the invariant should allow anything but <span class="user-mention" data-user-id="123856">@Vadim Petrochenkov</span> thinks we should have some invariant even here. Trait object pointers must have a valid vtable. And so on.</p>



<a name="131156351"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131156351" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131156351">(Aug 09 2018 at 07:42)</a>:</h4>
<p>The reason I think not putting "dereferencable" here is that this falls out of my aliasing model: Whenever you load a reference, it gets activated and retagged. That is UB if the reference is not dereferencable.</p>



<a name="131175103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131175103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131175103">(Aug 09 2018 at 14:18)</a>:</h4>
<p>No, there's a difference between "values" and "objects"</p>



<a name="131175127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131175127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131175127">(Aug 09 2018 at 14:19)</a>:</h4>
<p>it's like, the value 5 vs the box that 5 gets put in</p>



<a name="131175239"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131175239" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131175239">(Aug 09 2018 at 14:21)</a>:</h4>
<p>I recommend the book Elements of Programming, it goes over all of this stuff</p>



<a name="131177514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131177514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131177514">(Aug 09 2018 at 14:57)</a>:</h4>
<p>Like, here's an illustration of the idea:</p>
<p>Given a builtin type <code>T</code>, there exists a set of valid values for <code>T</code>; for a <code>bool</code>, that would be <code>{true,  false}</code>, for <code>i32</code>, that would be <code>[-2**31, 2**31) ∩ ℤ</code>, etc.</p>
<p>Given a <code>struct</code> or <code>tuple</code> (hereafter referred to as a product) type <code>T</code>, there exists a set of valid values for <code>T</code> which is constructed by taking the tuple of it's members - i.e., for <code>(bool, bool)</code> that would be the set <code>bool * bool</code>, or <code>{(true, true), (true, false), (false, true), (false, false)}</code></p>
<p>(continued)</p>



<a name="131178500"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131178500" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131178500">(Aug 09 2018 at 15:12)</a>:</h4>
<p>Given a <code>union</code> or <code>enum</code> type <code>T</code>, hereafter referred to as a sum type, there exists a set of valid values for <code>T</code> which is constructed by either<br>
  - (for the <code>union</code>) taking the union of the values of the member types - i.e., <code>union { bool, i32 }</code> would be the set <code>{true, false} ∪ ([-2**31, 2**31) ∩ ℤ)</code>,<br>
  - (for the <code>enum</code>)<br>
    - given a mapping <code>nth_ctor : (ℕ ∩ [0, N)) → Type</code> (where <code>N</code> is the number of constructors for <code>T</code>)<br>
    - which is defined as the map from the ctor index to the product type of that ctor<br>
    - the valid values of <code>T</code> are the set <code>∪(i = 0 to N) {(i, v) | v ∈ nth_ctor(i)}</code></p>



<a name="131179491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131179491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131179491">(Aug 09 2018 at 15:28)</a>:</h4>
<p>Let's call this map from the type to the set of its values, <code>val : Type -&gt; Set Value</code></p>
<p>A <code>Bit</code> is the set of values <code>{X, 1, 0}</code>.</p>
<p><code>⊑ : List Bit * List Bit -&gt; Bool</code> is defined: <code>x ⊑ y</code> if and only if<br>
  - the lists have the same length, <code>N</code><br>
  - for each index <code>n ∈ [0, N) ∩ ℕ</code><br>
    - if <code>yₙ = 0</code>, then <code>xₙ = 0</code><br>
    - if <code>yₙ = 1</code>, then <code>xₙ = 1</code><br>
    - if <code>yₙ = X</code>, then <code>xₙ</code> can be any bit<br>
Note: this relation has the effect of saying whether <code>x</code> has the same value as <code>y</code>.</p>
<p>Then, there exists a mapping <code>bits : val(T) → (l: List Bit)</code> where <code>l</code> has size <code>size_of::&lt;T&gt;()</code> - note that there exists no guarantee of distinctness, due to references and unions.</p>
<p>An object <code>o</code> with type <code>T</code> also has a list of <code>Bit</code>s (of size <code>size_of::&lt;T&gt;()</code>). Let's call this list <code>repr : Object -&gt; List Bit</code>. An object <code>o</code> with type <code>T</code> is valid if and only if <code>∃v : val(T) s.t. repr(o) ⊑ bits(v)</code>.</p>



<a name="131187763"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131187763" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131187763">(Aug 09 2018 at 17:57)</a>:</h4>
<p>Not sure when I will have tome to digest all of this, but just one comment up front: The Box that you put 5 in is also a value. that value is a pointer/address/location in memory.<br>
it is entirely unnecessary to talk about objects here. no objects appear anywhere in any of my formal models. or maybe you are just using "object" as a term for "location in memory"?</p>



<a name="131192344"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131192344" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131192344">(Aug 09 2018 at 19:20)</a>:</h4>
<p>Yes, an object is a location in memory with space for a value. You have to separate them when discussing mutation</p>



<a name="131192370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/131192370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#131192370">(Aug 09 2018 at 19:21)</a>:</h4>
<p>You also have things like this:</p>
<div class="codehilite"><pre><span></span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="k">i32</span><span class="p">;</span><span class="w"></span>
<span class="o">*</span><span class="p">((</span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">x</span><span class="p">)</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="p">[</span><span class="kt">u8</span><span class="p">;</span><span class="w"> </span><span class="mi">4</span><span class="p">])</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="p">[</span><span class="mi">0</span><span class="p">,</span><span class="w"> </span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="mi">2</span><span class="p">,</span><span class="w"> </span><span class="mi">3</span><span class="p">];</span><span class="w"></span>
</pre></div>


<p>which do type punning on a single object.</p>
<p>If you don't have locations with values in them, how do you have mutation?</p>
<div class="codehilite"><pre><span></span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span><span class="w"></span>
<span class="n">x</span><span class="w"> </span><span class="o">+=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
</pre></div>


<p><code>x</code> is one location, but it has both <code>0</code> and <code>1</code> in it at different times.</p>



<a name="132006934"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132006934" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132006934">(Aug 12 2018 at 18:35)</a>:</h4>
<p>Yeah, this distinction becomes important if we think about where it is legal to have a pointer (which indicates a location) pointing to an invalid value.</p>



<a name="132007021"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007021" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007021">(Aug 12 2018 at 18:38)</a>:</h4>
<p>If we're talking about bits as the set of valid values, then a 0 reference is definitely invalid. An unaligned reference should be invalid as well.</p>



<a name="132007024"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007024" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007024">(Aug 12 2018 at 18:38)</a>:</h4>
<p>We could require raw pointers be aligned as well, but I don't think it makes a big difference one way or the other.</p>



<a name="132007039"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007039" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007039">(Aug 12 2018 at 18:39)</a>:</h4>
<p>(also by "0 reference" I mean the null value, which may or may not be all-bits-0)</p>



<a name="132007131"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007131" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007131">(Aug 12 2018 at 18:42)</a>:</h4>
<p>If we make it a data layout invariant that fields are <em>always</em> nonoverlapping (I mentioned this on github and have more thoughts on this: a compiler could pack, say, multiple <code>bool</code>s into one byte in a struct/array if it could prove that there was never any separate addressing of them. But this could just be done by the as-if rule anyway.), then any arbitrarily nested field can be referred to without necessarily needing the rest of the struct (or any nested one) to be valid.</p>



<a name="132007136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007136">(Aug 12 2018 at 18:42)</a>:</h4>
<p>Likewise individual fields can be loaded without requiring validity of the others.</p>



<a name="132007145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007145">(Aug 12 2018 at 18:43)</a>:</h4>
<p>I can't think of any inherent reason we need to think of structs as being valid or invalid in toto.</p>



<a name="132007291"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007291" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007291">(Aug 12 2018 at 18:48)</a>:</h4>
<p>You can refer to them safely without any problems. You can even move them around, and you still don't actually run into any problems. As long as you don't try to actually access a field or do anything conditional on it, I don't think that we can have any issues there. The only thing I can think of is if the compiler does an oversize load <em>and</em> relies on the validity of the extra memory loaded to perform some tricky optimization (e.g. for a boolean, knowing that only one bit is set,  so ANDing against something you know has the bit cleared will always produce zeroes). I'm not sure if that is worth keeping the door open to.</p>



<a name="132007297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007297">(Aug 12 2018 at 18:49)</a>:</h4>
<p>Actually I guess the most likely case I can think of that is if I have, e.g.:</p>
<div class="codehilite"><pre><span></span><span class="k">enum</span> <span class="nc">Singleton</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="n">Variant</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">,</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
<span class="k">struct</span> <span class="nc">Thing</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="n">b</span>: <span class="kt">bool</span><span class="p">,</span><span class="w"></span>
<span class="w">  </span><span class="n">s</span>: <span class="nc">Singleton</span><span class="p">,</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">some_size</span><span class="p">(</span><span class="n">t</span>: <span class="nc">Thing</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kt">usize</span> <span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="k">if</span><span class="w"> </span><span class="n">t</span><span class="p">.</span><span class="n">b</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="mi">5</span><span class="w"></span>
<span class="w">  </span><span class="p">}</span><span class="w"> </span><span class="k">else</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="mi">91</span><span class="w"></span>
<span class="w">  </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>The compiler here might rely on <code>t.s</code> necessarily having value 0 in order to do an oversized load and then compare to 0. If this is an optimization we permit, then we have to define loading at the entire struct level, so that accessing a field for a load also loads the rest of the struct.</p>



<a name="132007452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007452">(Aug 12 2018 at 18:55)</a>:</h4>
<p>But then that rapidly becomes complicated if we consider that the load might happen deep in some other function: if, say, we pass <code>&amp;t.b</code> into another function, and then that loads from it, could the compiler inline and then do the oversize load? What if raw pointers were involved?</p>
<p>So my temptation here is to say that the compiler cannot rely on invariants in values in oversized loads.</p>



<a name="132007663"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007663" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007663">(Aug 12 2018 at 19:02)</a>:</h4>
<p>Enum layout optimizations do prevent us from allowing <code>*p = v</code> where <code>v</code> is invalid, but I don't think that applies for a fully-owned value. So <code>ptr::read</code> could read an invalid value safely if we wanted?</p>



<a name="132007670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007670">(Aug 12 2018 at 19:03)</a>:</h4>
<p>(provided that the result's invalid fields were not conditioned on, ofc)</p>



<a name="132007825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007825">(Aug 12 2018 at 19:08)</a>:</h4>
<p>But that may prove untenable in practice? not sure</p>



<a name="132007827"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132007827" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132007827">(Aug 12 2018 at 19:09)</a>:</h4>
<p>worth thinking about that, though</p>



<a name="132659124"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659124" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659124">(Aug 23 2018 at 20:34)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> I think bringing up some kind of denotational semantics for values like you are doing here is entirely unnecessary. in fact, from all I know, it is an unsolved problem to scale this to higher-order imperative languages. you'd have to explain "values" that makes up the function space, and then you run into recursive domain equation that you cannot solve... and much later you end up with essentially something like logical relations, where you do not need that abstract set of values at all. but anyway that is entirely off-topic, all we are discussion here is basic data layout invariants.</p>



<a name="132659149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659149">(Aug 23 2018 at 20:35)</a>:</h4>
<p>these invariants are on values represented in memory, i..e, sequences of bytes -- where a "byte" is the byte of an abstract machine that keeps track of extra state like whether something is initialized.</p>



<a name="132659221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659221">(Aug 23 2018 at 20:36)</a>:</h4>
<blockquote>
<p>If you don't have locations with values in them, how do you have mutation?</p>
</blockquote>
<p>oh, we totally have locations, and we have a memory that maps locations to bytes. I know C uses the term object for some of this, but I think it is rather confusing as we are not talking about OOP.</p>



<a name="132659254"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659254" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659254">(Aug 23 2018 at 20:37)</a>:</h4>
<p>also, we are unlikely to adopt C's extremely complicated object model. In LLVM, locations form a mostly "flat" address space -- separate allocations are distinguished, but you can do pointer arithmetic within an allocation across what C would call object boundaries</p>



<a name="132659281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659281">(Aug 23 2018 at 20:37)</a>:</h4>
<p><span class="user-mention" data-user-id="123893">@alercah</span> every <code>bool</code> can have its address taken so you cannot really change how an individual bool looks</p>



<a name="132659286"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659286" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659286">(Aug 23 2018 at 20:37)</a>:</h4>
<p><code>(bool, bool)</code> must always be 2 bytes</p>



<a name="132659497"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659497" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659497">(Aug 23 2018 at 20:42)</a>:</h4>
<p>So, coming back to memory, locations and objects -- I am coming at this from the perspctive that before you do anything else, you should define your state. C never does that, and it's a horrible mistake. that state will likely have some big finite partial function <code>location -fin&gt; byte</code> -- where both <code>location</code> and <code>byte</code>  don't have to be the "obvious" choice. in a boring IR, you could pick <code>location = u64</code> and <code>byte = u8</code>. in miri, we have <code>location = (AllocId, Offset)</code> and <code>byte</code> basically an enum <code>Initialized(u8), Uninit</code>, except we add some extra stuff to be able to also store pointers in memory. so on paper I would use <code>byte = enum { Data(u8), Uninit, PtrFragment { ptr: location, idx: u8 }</code> where <code>PtrFragment(ptr, n)</code> represents byte <code>n</code> of a pointer. the only reason we do not have that in miri is performance.</p>



<a name="132659553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132659553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132659553">(Aug 23 2018 at 20:42)</a>:</h4>
<p>so then, based on that, the validity invariant is a predicate over <code>byte^n</code> -- and maybe it can also depend on the current state of memory.</p>



<a name="132704491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132704491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132704491">(Aug 24 2018 at 16:19)</a>:</h4>
<p>How C does this is that functions are not object - in fact, Rust is the same way. A function is fundamentally different from an object. That's why we have <code>&amp;T</code> and <code>fn()</code></p>



<a name="132704550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132704550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132704550">(Aug 24 2018 at 16:21)</a>:</h4>
<p>A function doesn't have a value in the classical sense, in systems languages</p>



<a name="132704567"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132704567" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132704567">(Aug 24 2018 at 16:21)</a>:</h4>
<p>Also, "object" for "location + value" is a common wording in systems languages, and I feel it's unnecessary to reinvent the wheel when it comes to language here</p>



<a name="132707064"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132707064" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132707064">(Aug 24 2018 at 17:13)</a>:</h4>
<p>location + value? as in, the value stored at that location?</p>



<a name="132707109"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132707109" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132707109">(Aug 24 2018 at 17:14)</a>:</h4>
<p>however that only makes sense when you also consider types. otherwise you do not know how many bytes to consider.</p>



<a name="132707112"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132707112" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132707112">(Aug 24 2018 at 17:14)</a>:</h4>
<p>and memory is better treated as inherently untyped.</p>



<a name="132709799"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709799" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709799">(Aug 24 2018 at 18:01)</a>:</h4>
<p>Yea, but lvalues are inherently typed</p>



<a name="132709933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709933">(Aug 24 2018 at 18:02)</a>:</h4>
<p>hm, no, I dont think so. in miri we have <code>Place</code> and it is not typed by itself. we often carry it along with its type information, but the concept makes sense without types.</p>



<a name="132709964"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709964" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709964">(Aug 24 2018 at 18:03)</a>:</h4>
<p>well, a Place is an "expression", essentially, in some context, so you can compute its type?</p>



<a name="132709974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709974">(Aug 24 2018 at 18:03)</a>:</h4>
<p>I was talking about <code>miri::Place</code>, not <code>mir::Place</code></p>



<a name="132709975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709975">(Aug 24 2018 at 18:03)</a>:</h4>
<p>or maybe miri means something distinct from MIR when you say <code>Place</code></p>



<a name="132709979"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132709979" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132709979">(Aug 24 2018 at 18:04)</a>:</h4>
<p>i.e. the thing the expression computes to</p>



<a name="132710016"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710016" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710016">(Aug 24 2018 at 18:04)</a>:</h4>
<p>I see, ok</p>



<a name="132710021"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710021" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710021">(Aug 24 2018 at 18:04)</a>:</h4>
<p>which is essentially a location + alignment + info for unsized stuff</p>



<a name="132710035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710035">(Aug 24 2018 at 18:04)</a>:</h4>
<p>but to be fair I think we have hardly any use in miri for a place without a type</p>



<a name="132710047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710047">(Aug 24 2018 at 18:05)</a>:</h4>
<p>but that's because places are an "ephemeral" concept -- they exist during evluation of a statement, but are not really part of the machine state</p>



<a name="132710049"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710049" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710049">(Aug 24 2018 at 18:05)</a>:</h4>
<p>so you're saying you have <code>void*</code> for all lvalues, and each read is <code>read(type, offset, lvalue)</code>?</p>



<a name="132710062"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710062" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710062">(Aug 24 2018 at 18:05)</a>:</h4>
<p>or something along those lines?</p>



<a name="132710076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710076">(Aug 24 2018 at 18:05)</a>:</h4>
<p>when you want to actually read you need a size, yes. not a full type though.</p>



<a name="132710082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710082">(Aug 24 2018 at 18:05)</a>:</h4>
<p>(miri needs a type for reasons that are only related to optimizations)</p>



<a name="132710159"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710159" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710159">(Aug 24 2018 at 18:06)</a>:</h4>
<p>that seems like a very odd model</p>



<a name="132710171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710171">(Aug 24 2018 at 18:06)</a>:</h4>
<p>values... should... be typed</p>



<a name="132710211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710211">(Aug 24 2018 at 18:07)</a>:</h4>
<p>no I dont think so. types only matter when you are actually computing.</p>



<a name="132710230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710230">(Aug 24 2018 at 18:08)</a>:</h4>
<p>and even then, I'd make <code>unsigned-mul</code> and <code>signed-mul</code> just different operations</p>



<a name="132710278"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710278" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710278">(Aug 24 2018 at 18:08)</a>:</h4>
<p>and then both can work on untyped bytes</p>



<a name="132710281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710281">(Aug 24 2018 at 18:08)</a>:</h4>
<p>I... really dislike that model</p>



<a name="132710302"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710302" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710302">(Aug 24 2018 at 18:08)</a>:</h4>
<p>I think types are just making trouble on this level</p>



<a name="132710314"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710314" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710314">(Aug 24 2018 at 18:08)</a>:</h4>
<p>I don't agree at all</p>



<a name="132710319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710319">(Aug 24 2018 at 18:08)</a>:</h4>
<p>types should be used to <em>reason about</em> program behavior, not to <em>define</em> program behavior</p>



<a name="132710323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710323">(Aug 24 2018 at 18:09)</a>:</h4>
<p>but I appreciate that this is an opinion :)</p>



<a name="132710479"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710479" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710479">(Aug 24 2018 at 18:11)</a>:</h4>
<p>and I can live with types being used during the evaluation of a single expression -- as long as the machine state that is kept from one evaluation step to the next does not have types</p>



<a name="132710628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710628">(Aug 24 2018 at 18:13)</a>:</h4>
<p>I would argue that, for example, <code>fn () -&gt; i32</code> should actually return <code>i32</code> in the model, and not just "4 bytes"</p>



<a name="132710645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710645">(Aug 24 2018 at 18:13)</a>:</h4>
<p>and similarly, that <code>fn (i32) -&gt; i32</code> should be callable only with <code>i32</code></p>



<a name="132710647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710647">(Aug 24 2018 at 18:13)</a>:</h4>
<blockquote>
<p>values... should... be typed</p>
</blockquote>
<p>I mean -- values can have multiple types, clearly... (union, transmute). So you have to reconcile for that at minimum. This does tend to lead you towards Ralf's POV</p>



<a name="132710713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710713">(Aug 24 2018 at 18:14)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I very much disagree</p>



<a name="132710729"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710729" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710729">(Aug 24 2018 at 18:14)</a>:</h4>
<p>although <span class="user-mention" data-user-id="120791">@RalfJ</span> I'd still like to understand how transmute plays with the ref tracking in stacked borrows =)</p>



<a name="132710734"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710734" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710734">(Aug 24 2018 at 18:14)</a>:</h4>
<p><code>union</code> and <code>transmute</code> do not have values of multiple types</p>



<a name="132710770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132710770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132710770">(Aug 24 2018 at 18:15)</a>:</h4>
<p><code>transmute</code> takes the object representation of one value, and gives you a value of a different type with the same object representation</p>



<a name="132711107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132711107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132711107">(Aug 24 2018 at 18:21)</a>:</h4>
<p>my favorite example where, imo, that kind of thinking breaks down, is with return values of struct type</p>
<p>given a type <code>struct i64x2 { x: i64, y: i64 }</code>, and a function <code>fn f() -&gt; i64x2 { i64x2 { x: 0, y: 0 } }</code>, there _does_ exist a value of type <code>i64x2</code>, but there never exists an _object_ of type <code>i64x2</code></p>



<a name="132711125"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132711125" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132711125">(Aug 24 2018 at 18:21)</a>:</h4>
<p>(assuming x64 ABI)</p>



<a name="132711145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132711145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132711145">(Aug 24 2018 at 18:21)</a>:</h4>
<p>you don't ever actually have a <code>byte ^ 16</code> thing</p>



<a name="132726543"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132726543" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132726543">(Aug 25 2018 at 00:03)</a>:</h4>
<p>ABIs are implementation details though, for language semantics it seems absolutely fine -- even desirable for simplicity -- that every function writes its result to a place that is passed in (and indeed this is how MIR currently works)</p>



<a name="132727047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132727047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132727047">(Aug 25 2018 at 00:21)</a>:</h4>
<p>why is that more simple than "returns a value"</p>



<a name="132728540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132728540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132728540">(Aug 25 2018 at 01:08)</a>:</h4>
<p>it is also true that computer hardware is not typed; so there is some advantage if you can map your model to types being something that the code "adds" to the base layer</p>



<a name="132728544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132728544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132728544">(Aug 25 2018 at 01:08)</a>:</h4>
<p>although the mapping between this base layer and hardware is...suggestive at best, I suppose :)</p>



<a name="132741312"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741312" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741312">(Aug 25 2018 at 08:58)</a>:</h4>
<p>I think <code>transmute</code> is just a NOP</p>



<a name="132741320"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741320" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741320">(Aug 25 2018 at 08:58)</a>:</h4>
<p>it copies bytes around, done</p>



<a name="132741322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741322">(Aug 25 2018 at 08:58)</a>:</h4>
<p>that thing with struct return value is entirely a platform implementation detail</p>



<a name="132741328"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741328" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741328">(Aug 25 2018 at 08:59)</a>:</h4>
<p>as far as language spec is concerned, a place exists somewhere that is prepared by the caller, and where the callee writes this return value into</p>



<a name="132741332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741332">(Aug 25 2018 at 08:59)</a>:</h4>
<p>and by "write the return value", I mean that it does <code>return_place.x = 0; return_place.y = 0;</code></p>



<a name="132741337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741337">(Aug 25 2018 at 09:00)</a>:</h4>
<p>or <code>return_place = i64x2 { ... }</code> if we have aggregate creation as primitive (which IIRC MIR has)</p>



<a name="132741385"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741385" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741385">(Aug 25 2018 at 09:00)</a>:</h4>
<blockquote>
<p>why is that more simple than "returns a value"</p>
<p>why is that more simple than "returns a value"</p>
</blockquote>
<p>we do not need the concept of a "value".</p>



<a name="132741393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741393">(Aug 25 2018 at 09:01)</a>:</h4>
<p>we have scalars, which is something we can immediately perform computation on; everything else just exists as place/operand in memory</p>



<a name="132741398"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741398" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741398">(Aug 25 2018 at 09:01)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> sorry it's not inherently simpler in itself, but it's one component (along with having places rather than just values in other parts of the language) of allowing us to avoid specifying validity for values, or more generally a really formalized denotational semantics</p>



<a name="132741399"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132741399" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132741399">(Aug 25 2018 at 09:01)</a>:</h4>
<p>no need to invent a concept of a "value" which is something like "a bunch of bytes, but not sitting in memory currently"</p>



<a name="132751978"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132751978" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132751978">(Aug 25 2018 at 15:05)</a>:</h4>
<p>I think the question is "what is the purpose of the model". If it's "allow people to reason about their Rust", I'd argue a typed semantics is far easier to reason about; if the question is "allow us to reason about the Rust model", then it might be better to have it be untyped. I personally think it's much easier to reason about unsafe code which has values and types, not buffers and invariants.</p>



<a name="132752149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752149">(Aug 25 2018 at 15:10)</a>:</h4>
<p>quite a few of the tricky questions that people writing unsafe/systems-y code ask are naturally about memory contents: can i type pun this buffer, is this layout compatible with C, can i read this uninitialized memory and do X with it, etc. so i don't really see how a typed-values-first approach will be automatically more natural</p>



<a name="132752212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752212">(Aug 25 2018 at 15:10)</a>:</h4>
<p>that's kind of the less interesting parts of unsafe code, imo</p>



<a name="132752298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752298">(Aug 25 2018 at 15:13)</a>:</h4>
<p>maybe it's just due to being in the C++ community, where we have a value based semantics and it's very useful (and fairly reasonable) to read the standard</p>



<a name="132752407"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752407" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752407">(Aug 25 2018 at 15:16)</a>:</h4>
<p>it also more closely matches the actual machine, imo</p>



<a name="132752411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752411">(Aug 25 2018 at 15:16)</a>:</h4>
<p>we really aren't dealing with memory, most of the time; we're dealing with registers (which are different depending on type!)</p>



<a name="132752473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752473">(Aug 25 2018 at 15:18)</a>:</h4>
<p>i think this is a red herring, despite 90% of my compiler work dealing intimately with these sorts of Real Machine Widgets<br>
a language definition needs to <em>permit</em> efficient compilation, but it doesn't need to be very suggestive of that compilation strategy, especially since any analogy to real machines will likely be superficial anyway</p>



<a name="132752503"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752503" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752503">(Aug 25 2018 at 15:19)</a>:</h4>
<p>aside: if one really wanted a language semantics tailored to register machines, it would be more useful to give up the pretense that certain kinds of values (e.g., condition codes, masks, <em>variable-length</em> vectors) can be stored in memory _at all_</p>



<a name="132752540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752540">(Aug 25 2018 at 15:20)</a>:</h4>
<p>sure</p>



<a name="132752560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132752560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132752560">(Aug 25 2018 at 15:20)</a>:</h4>
<p>I don't disagree with that idea lol</p>



<a name="132753034"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/132753034" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#132753034">(Aug 25 2018 at 15:36)</a>:</h4>
<p>also, obviously this is all opinion, and Ralf's model is also entirely valid; I just think a value-based model is easier to understand (due to being super familiar with them with C++)</p>



<a name="133111745"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133111745" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133111745">(Aug 31 2018 at 08:42)</a>:</h4>
<blockquote>
<p>maybe it's just due to being in the C++ community, where we have a value based semantics and it's very useful (and fairly reasonable) to read the standard</p>
</blockquote>
<p>You are the first person that I hear say such things about C++.^^ I consider the C++ standard to be huge and unreadable... and also fundamentally deficient because it is not written int he style of an "abstract machine". C++ is axiomatic, it essentially says "I wish all these things to be true" and then leaves it to others to figure out if, and how, that is possible.</p>
<p>All the work for actually reasoning formally about low-level code that I am ware of (first and foremost, CompCert) uses an untyped memory. Types make it harder to define what your machine is, and a more complicated machine is more complicated to reason about.</p>



<a name="133111860"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133111860" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133111860">(Aug 31 2018 at 08:45)</a>:</h4>
<p>So, I think the purpose of this exercise is to <em>define</em> Rust, and a definition should be (a) executable, written with some form of abstract machine in mind, because that's how people think about their programs, and (b) as simple as possible. The latter is crucially important also when reasoning about your code.</p>
<p>Registers are entirely an implementation detail. No need to clutter our language definition with such concerns.</p>



<a name="133111968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133111968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133111968">(Aug 31 2018 at 08:47)</a>:</h4>
<p>That said, I know plenty of people who consider axiomatic models useful and maybe even superior to the operational approach I am proposing. There is certainly a large amount of personal preference in there, and it probably also depends on what you are doing. However, the history of UB in C/C++ IMHO shows that having only an axiomatic definition is not sufficient -- clearly, the axiomatic definition of C/C++ did not really help programmers to determine if their code is UB; in fact, even compiler authors and academics struggle to make sense out of it. I think that is a piece of hard evidence against such an axiomatic approach.</p>



<a name="133112047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133112047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133112047">(Aug 31 2018 at 08:49)</a>:</h4>
<p>Also see <a href="https://blog.regehr.org/archives/1520" target="_blank" title="https://blog.regehr.org/archives/1520">John Regehr advocating an operational definition</a>, and <a href="https://lkml.org/lkml/2018/6/7/761" target="_blank" title="https://lkml.org/lkml/2018/6/7/761">even Torvalds agrees</a>.<br>
Another piece of evidence is the story of weak memory models: Initially they were all axiomatic, but none of them managed to solve the "out of thin air" problem. one of the best contenders we have right now is the <a href="https://people.mpi-sws.org/~viktor/papers/popl2017-promising.pdf" target="_blank" title="https://people.mpi-sws.org/~viktor/papers/popl2017-promising.pdf">first realistic *operational* model of relaxed memory</a>.</p>



<a name="133112233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133112233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133112233">(Aug 31 2018 at 08:53)</a>:</h4>
<p>I am not debating that a higher-level view is useful for reasoning, that's why I am working on program logics for my PhD. ;) but the gold standard here is to <em>prove</em> that your value-based fiction is actually correct with respect to a more low-level operational semantics. Thus we end up with a semantics that is reasonably close to "the real thing" (where "reasonable" of course depends on your PoV^^) -- LLVM's memory is untyped and just a "bunch of bytes", which is important because we have to <em>trust</em> that the semantics match what really happens. And we still get high-level reasoning, but in a way that we know is sound because there is a proof connecting it to the low-level "reality" (just another model, of course, but hopefully one that is much easier to declare realistic).</p>



<a name="133112448"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133112448" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133112448">(Aug 31 2018 at 08:56)</a>:</h4>
<p>In most of my work, when I am not interested in pointer arithmetic or layout concerns, we have a very high-level view of memory where the "value" you can store in a location can be arbitrarily big, contain nested sums and products and closures and whatnot. We put all the burden on implementing this on the compiler. But that is not so hard because there is no pointer arithmetic and no transmute, there is no way for the program to observe what the compiler is doing. But if you'd now want to also define, <em>in the same language</em>, what happens with byte-level accesses -- that's where I have yet to see a high-level model that I would actually trust to match actual program behavior. (And it is about trust here, this is the fundamental definition of the language and we do not have a verified compiler.) <a href="https://robbertkrebbers.nl/thesis.html" target="_blank" title="https://robbertkrebbers.nl/thesis.html">Robbert Krebber's thesis</a> is the closest I know, and it is very far from "simple".</p>



<a name="133112704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133112704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133112704">(Aug 31 2018 at 09:01)</a>:</h4>
<p>Sorry for the long rant, I felt I had to explain where I am coming from.^^</p>
<p>Do you know of a <em>simple</em> explanation of C++'s value-based model? Simple means it easily fits onto a dozen pages or so, but should still support some amount of both byte-level and high-level operations and give a precise description of what is UB. All I hear from my peers is hardly anyone tried formalizing C++ because it is so complicated.</p>
<p><a href="https://hal.inria.fr/hal-00703441/document" target="_blank" title="https://hal.inria.fr/hal-00703441/document">Here's a rather simple but realistic untyped model for a subset of C</a>. "Simple" because it fits in a paper -- it's almost 3 dozen pages but it's also giving lots of background and related work and so on. And "realistic" because it is the one used by CompCert to compile plenty of actual C code. It even provides some facilities for concurrent execution (just with locks, but still).</p>



<a name="133113288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133113288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133113288">(Aug 31 2018 at 09:14)</a>:</h4>
<p>(The fact that there is hardly any formal work on reasoning about C++ also seems to contradict your statement that C++'s definition is well-suited for reasoning.)</p>



<a name="133126332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Basile Desloges <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126332">(Aug 31 2018 at 14:08)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> I thought the C++ spec was written against an abstract machine (from <a href="https://www.youtube.com/watch?v=KoqY50HSuQg" target="_blank" title="https://www.youtube.com/watch?v=KoqY50HSuQg">https://www.youtube.com/watch?v=KoqY50HSuQg</a> slide 18, I tried to retrieve the source directly but the page seems to have changed and I can't find it :/). Did something changed since that video or are you speaking of something else?</p>
<div class="youtube-video message_inline_image"><a data-id="KoqY50HSuQg" href="https://www.youtube.com/watch?v=KoqY50HSuQg" target="_blank" title="https://www.youtube.com/watch?v=KoqY50HSuQg"><img src="https://i.ytimg.com/vi/KoqY50HSuQg/default.jpg"></a></div>



<a name="133126577"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126577" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126577">(Aug 31 2018 at 14:12)</a>:</h4>
<p>The C++ standard, at least every edition I have seen so far, is written like the C standard</p>



<a name="133126582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126582">(Aug 31 2018 at 14:13)</a>:</h4>
<p>and that's as far away from an abstract machine as it gets</p>



<a name="133126589"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126589" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126589">(Aug 31 2018 at 14:13)</a>:</h4>
<p>but if I am wrong with that, that'd be great :D</p>



<a name="133126610"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126610" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Basile Desloges <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126610">(Aug 31 2018 at 14:13)</a>:</h4>
<p>You mean the way the standard is written then? Maybe it <em>is</em> written against an abstract machine, but not very clearly :)</p>



<a name="133126768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126768">(Aug 31 2018 at 14:16)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> may be referring to the difference between an axiomatic definition (list of guarantees, but without directly describing how the abstract machine behaves) and an operational definition (which directly gives you an algorithm you can execute)</p>



<a name="133126869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Basile Desloges <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126869">(Aug 31 2018 at 14:18)</a>:</h4>
<p>Oh I see thanks. I think I didn't really understood the difference between those two :)</p>



<a name="133126899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126899">(Aug 31 2018 at 14:19)</a>:</h4>
<p>Well, I have not seen anything resembling a definition of an abstract machine, which starts by saying: here's the machine <em>state</em>, and then here's the possible execution steps and how they manipulate said state.</p>



<a name="133126916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133126916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133126916">(Aug 31 2018 at 14:19)</a>:</h4>
<p>maybe the authors had an abstract machine in mind, but never told us about it. But for C, writing a conforming abstract machine didn't happen until &lt;5 years ago in academia (it's still not normative, and it's huge and almost unusable for reasoning or any other purpose, really; but it's a start). And C++ is much harder.</p>



<a name="133130004"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133130004" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133130004">(Aug 31 2018 at 15:16)</a>:</h4>
<p>It's a very <em>abstract</em> abstract machine</p>



<a name="133134200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134200">(Aug 31 2018 at 16:40)</a>:</h4>
<p>I don't mean reasoning in a "you" sort of way, I mean reasoning in a "user" sort of way. Also, LLVM doesn't have the model of untyped memory; it has a C++ style memory + values model?</p>



<a name="133134208"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134208" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134208">(Aug 31 2018 at 16:41)</a>:</h4>
<blockquote>
<p><a href="https://hal.inria.fr/hal-00703441/document" target="_blank" title="https://hal.inria.fr/hal-00703441/document">Here's a rather simple but realistic untyped model for a subset of C</a></p>
</blockquote>
<p>Nice citation.</p>



<a name="133134294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134294">(Aug 31 2018 at 16:43)</a>:</h4>
<p>Also, here's the base model of C++: <a href="http://eel.is/c++draft/basic.memobj" target="_blank" title="http://eel.is/c++draft/basic.memobj">http://eel.is/c++draft/basic.memobj</a></p>



<a name="133134301"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134301" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134301">(Aug 31 2018 at 16:43)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> I think reasoning in a "user" sort of way is misguided and likely incorrect if it cannot be put on solid formal foundations.</p>



<a name="133134309"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134309" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134309">(Aug 31 2018 at 16:43)</a>:</h4>
<p>and no from all I see in the lang ref, LLVM's memory is entirely untyped</p>



<a name="133134317"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134317" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134317">(Aug 31 2018 at 16:44)</a>:</h4>
<p>it doesnt "remember" at which type bytes were put unto it</p>



<a name="133134358"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134358" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134358">(Aug 31 2018 at 16:44)</a>:</h4>
<p>also all the formal models I have seen for LLVM use untyped memory</p>



<a name="133134390"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134390" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134390">(Aug 31 2018 at 16:45)</a>:</h4>
<p>whereas for C, Robbert Krebber's thesis is an example of a formal "kind-of typed"(?) memory. at least, structs and arrays are visible as such in memory.</p>



<a name="133134397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134397">(Aug 31 2018 at 16:45)</a>:</h4>
<p>whereas for LLVM, structs and arrays are only relevant to compute the address of an access. memory is "flat".</p>



<a name="133134464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134464">(Aug 31 2018 at 16:46)</a>:</h4>
<p>I will stash these C++ references somewhere for consumption after my vacation :)</p>



<a name="133134478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134478">(Aug 31 2018 at 16:46)</a>:</h4>
<div class="codehilite"><pre><span></span>define i32 @main() {
start:
  %0 = i32 0
  ret i32 %0
}
</pre></div>


<p>^ note that <code>%0</code> has type <code>i32</code></p>



<a name="133134486"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134486" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134486">(Aug 31 2018 at 16:46)</a>:</h4>
<p>_memory_ doesn't have a type, but _values_ do</p>



<a name="133134615"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133134615" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133134615">(Aug 31 2018 at 16:49)</a>:</h4>
<p>(which is what I'm arguing for)</p>



<a name="133135729"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133135729" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133135729">(Aug 31 2018 at 17:09)</a>:</h4>
<blockquote>
<p>I don't mean reasoning in a "you" sort of way, I mean reasoning in a "user" sort of way. </p>
</blockquote>
<p>I'm a bit curious about this — my impression is that many unsafe code authors (myself included) would prefer to have an underlying "untyped" model that they can reason about. The farther things get from how the underlying computer works (or at least the simple abstaction we have for it), the more confusing things are. Witness e.g. the common attempt to disable type-based aliasing etc, because it is hard to figure out if code is obeying those rules.</p>
<p>I don't have real data on this, of course, and you seem to have the exact opposite impression. I could easily imagine that there are people who have the reverse opinion. It might be interesting to take some "case study" examples that highlight the differences and try to see what falls about from thinking through them in both "styles". I'm not sure exactly what that means =)</p>



<a name="133135905"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133135905" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133135905">(Aug 31 2018 at 17:12)</a>:</h4>
<blockquote>
<p>_memory_ doesn't have a type, but _values_ do</p>
</blockquote>
<p>Well that's already much less typed than I thought you would advocate. :)<br>
my argument, then, is that the value on the types solely serves to select the right operation. <em>operations</em> are typed, because it makes a difference whether you multiply signed or unsigned integers.</p>



<a name="133135933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133135933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133135933">(Aug 31 2018 at 17:12)</a>:</h4>
<p>but depending on what you mean by "values", they do not even exist very long -- in miri, "values" only exist to be fed into operations</p>



<a name="133135950"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133135950" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133135950">(Aug 31 2018 at 17:13)</a>:</h4>
<p>but between two execution steps, there is no notion of a "value"</p>



<a name="133135965"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133135965" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133135965">(Aug 31 2018 at 17:13)</a>:</h4>
<p>there is memory (allocations containing bytes), and a stack where the local variables are also just an allocation ID saying where in memory this local is stored.</p>



<a name="133136019"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136019" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136019">(Aug 31 2018 at 17:14)</a>:</h4>
<p>so if the "values" you speak of are a mostly ephemeral concept, I think we are actually pretty close.</p>



<a name="133136055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136055">(Aug 31 2018 at 17:14)</a>:</h4>
<p>however, we do not really need anything other than primitive types to type those values, as primitive operations only act on primitive types</p>



<a name="133136106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136106">(Aug 31 2018 at 17:15)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> there is actually research that tries to find out what people <em>think</em> C is, that might be relevant... let me see if I can find it</p>



<a name="133136119"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136119" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136119">(Aug 31 2018 at 17:15)</a>:</h4>
<p>ah yes I think I've seen it</p>



<a name="133136122"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136122" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136122">(Aug 31 2018 at 17:15)</a>:</h4>
<p>but would like to see it again :)</p>



<a name="133136162"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136162" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136162">(Aug 31 2018 at 17:16)</a>:</h4>
<p>I think that would be <a href="https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html" target="_blank" title="https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html">https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html</a></p>



<a name="133136189"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136189" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136189">(Aug 31 2018 at 17:16)</a>:</h4>
<p>and more general the Cerberus project is a good source of C-related information: <a href="https://www.cl.cam.ac.uk/~pes20/papers/topics.html#Cerberus" target="_blank" title="https://www.cl.cam.ac.uk/~pes20/papers/topics.html#Cerberus">https://www.cl.cam.ac.uk/~pes20/papers/topics.html#Cerberus</a></p>



<a name="133136666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136666">(Aug 31 2018 at 17:26)</a>:</h4>
<p>yeah, you only should care about the type of values when you're using them; in that case, you do need full nominal types, if only because <code>struct A { x: i32, y: f32 }</code> and <code>struct B { x: i32, y: f32 }</code> aren't guaranteed to be layed out the same</p>



<a name="133136762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136762">(Aug 31 2018 at 17:28)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> my experience is with C++ people. C people are very different from C++ people, ime</p>



<a name="133136782"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136782" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136782">(Aug 31 2018 at 17:29)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> did you read my initial idea for a model &gt;.&lt;</p>



<a name="133136850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133136850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133136850">(Aug 31 2018 at 17:30)</a>:</h4>
<p>I absolutely don't think that memory should be typed, and I've argued that we (in this case meaning the C++ community) should change the C++ model to have untyped memory as well</p>



<a name="133147632"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133147632" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133147632">(Aug 31 2018 at 20:47)</a>:</h4>
<p>you never really do anything with "value" of struct type, other than copying them around, for which you only need the size. so those types are not actually relevant, all we need is size annotations at copy operations. the only place where we need full types is for primitive operations -- arithmetic and the like. (these types are extremely relevant for <em>layout</em> concerns, of course, but I see that as mostly separate -- layout fixes the offsets of all the fields; the main semantics and memory model then say what happens for a given assignment of offsets.)</p>
<p>I have seen an idea for a model of yours last year, yes -- but I did not get very far understanding it. :/ it started out introducing a huge host of terminology, and I was lost in that jungle of definitions before it even really started.</p>



<a name="133151388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151388">(Aug 31 2018 at 22:09)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> that's not necessarily true - for example, <code>Box&lt;T&gt;</code> should always be non-zero when it's a value</p>



<a name="133151458"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151458" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151458">(Aug 31 2018 at 22:11)</a>:</h4>
<p>what, specifically, do you mean by "when it's a value"? in particular, what does that cover that isn't covered by a non-null invariant on the bytes in memory, asserted e.g. when it's loaded?</p>



<a name="133151573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151573">(Aug 31 2018 at 22:14)</a>:</h4>
<p><span class="user-mention" data-user-id="124289">@rkruppe</span> that's exactly what I mean - <code>let x: Box&lt;i32&gt; = e;</code> &lt;- at the point when this statement is executed, <code>e</code> better evaluate to a non-null <code>Box&lt;i32&gt;</code> value</p>



<a name="133151762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151762">(Aug 31 2018 at 22:19)</a>:</h4>
<p>ok but that doesn't require defining values and deciding invariants for them, it seems to me you can just put enough things into memory that everything we care about is in memory at the time where we want to assert that it's valid</p>



<a name="133151788"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151788" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151788">(Aug 31 2018 at 22:19)</a>:</h4>
<p>wha..?</p>



<a name="133151892"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151892" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151892">(Aug 31 2018 at 22:21)</a>:</h4>
<p>however you want to put it, if you have <code>define void @foo(i32 * nonnull noalias)</code>, that <code>i32*</code> value has to be both nonnull and noalias; there is no memory there</p>



<a name="133151898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151898">(Aug 31 2018 at 22:21)</a>:</h4>
<p>for example in <code>let PAT = EXPR;</code> evaluation of <code>EXPR</code> writes the result to a temporary memory locations, and the <code>let</code> copies parts of that into named (and possibly longer-lived) memory locations</p>



<a name="133151960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133151960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133151960">(Aug 31 2018 at 22:22)</a>:</h4>
<p>once again, whatever we do at the LLVM IR level doesn't need to impact the language memory model, we only need to be able to justify the optimizations done on LLVM IR (including those made by the translation to LLVM IR)</p>



<a name="133152037"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152037" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152037">(Aug 31 2018 at 22:24)</a>:</h4>
<p>I don't think everything being memcpy's is especially understandable or useful, rather than just having values; it also ignores the reality of stuff like <code>let x = &amp;prvalue-expression;</code>, imo</p>



<a name="133152123"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152123" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152123">(Aug 31 2018 at 22:27)</a>:</h4>
<p>there is another angle to this -- we'll likely represent Box&lt;T&gt; just like any primitive pointer (e.g. as a scalar in miri), and can therefore do everything with this scalar that we do with other primitives, without introducing any value for "a struct containing a single pointer"</p>



<a name="133152187"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152187" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152187">(Aug 31 2018 at 22:28)</a>:</h4>
<p>or in other words, keeping the data model of the abstract machine limited to "scalars + untyped memory"</p>



<a name="133152215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152215">(Aug 31 2018 at 22:29)</a>:</h4>
<p><span class="user-mention" data-user-id="124289">@rkruppe</span> what about <code>Rc&lt;T&gt;</code>? What about some user-defined pointer type? what about <code>&amp;[T]</code>?</p>



<a name="133152262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152262">(Aug 31 2018 at 22:30)</a>:</h4>
<p>the _language_ doesn't say anything about invariants of Rc, does it? beyond what follows from the components that library code uses to create Rc</p>



<a name="133152271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152271">(Aug 31 2018 at 22:30)</a>:</h4>
<p>yes it does have invariants on Rc, that's what <code>std::ptr::Shared</code> is for</p>



<a name="133152280"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152280" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152280">(Aug 31 2018 at 22:31)</a>:</h4>
<p>that's what i meant with "what follows from the components"</p>



<a name="133152296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152296">(Aug 31 2018 at 22:31)</a>:</h4>
<p>also idk what you mean with "the reality of stuff like <code>let x = &amp;prvalue-expression;</code>" -- pretty much by definition that has to place the result of the prvalue-expression into memory?</p>



<a name="133152356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152356">(Aug 31 2018 at 22:32)</a>:</h4>
<p>it doesn't do any memory copies tho</p>



<a name="133152412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152412">(Aug 31 2018 at 22:33)</a>:</h4>
<p>yes, what's the problem? just evaluate the expression into a longer-lived stack slot (living as long as <code>x</code>) than for temporaries that live shorter</p>



<a name="133152480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152480">(Aug 31 2018 at 22:35)</a>:</h4>
<p>i'll also note, since you apparently care about proximity to the compiled code more than I do, that evaluating an aggregate will indeed directly write the fields to memory (unless the aggregate is very small), or at least it will once we have proper RVO/move forwarding on MIR</p>



<a name="133152489"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152489" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152489">(Aug 31 2018 at 22:35)</a>:</h4>
<p>yes, but it won't then copy it?</p>



<a name="133152499"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152499" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152499">(Aug 31 2018 at 22:35)</a>:</h4>
<p>it'll just write it to the stack slot</p>



<a name="133152550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152550">(Aug 31 2018 at 22:36)</a>:</h4>
<p>ok apparently we're talking past each other</p>



<a name="133152560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152560">(Aug 31 2018 at 22:36)</a>:</h4>
<p>when and where do you think i'm saying what exactly is copied?</p>



<a name="133152563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152563">(Aug 31 2018 at 22:37)</a>:</h4>
<p>and if we don't have a model beyond "builtins and untyped memory", what happens to <code>struct X { y: Unique&lt;T&gt;, z: i32 }</code>? <code>fn foo(x: X)</code> _requires_ that <code>x.y</code> is non-null</p>



<a name="133152581"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152581" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152581">(Aug 31 2018 at 22:37)</a>:</h4>
<blockquote>
<p>evaluation of EXPR writes the result to a temporary memory locations, and the let copies parts of that into named (and possibly longer-lived) memory locations</p>
</blockquote>



<a name="133152623"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152623" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152623">(Aug 31 2018 at 22:38)</a>:</h4>
<p>oh i forgot i put it like that</p>



<a name="133152624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152624">(Aug 31 2018 at 22:38)</a>:</h4>
<p>sorry</p>



<a name="133152648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152648">(Aug 31 2018 at 22:39)</a>:</h4>
<p>we very clearly have a value of type <code>X</code> getting passed to <code>foo</code> - we don't suddenly pass a memory buffer just because it's a UDT</p>



<a name="133152658"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152658" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152658">(Aug 31 2018 at 22:39)</a>:</h4>
<p>i can only plead again to separate the rules we impose on the language from the implementation</p>



<a name="133152707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152707">(Aug 31 2018 at 22:40)</a>:</h4>
<p>also at least if you add another i32 field we will, in fact, create LLVM IR that passes the aggregate in memory</p>



<a name="133152708"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152708" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152708">(Aug 31 2018 at 22:40)</a>:</h4>
<p>yes, the implementation would differ based on what ABI you're targeting</p>



<a name="133152715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152715">(Aug 31 2018 at 22:40)</a>:</h4>
<p>you would literally pass a pointer to an <code>X</code> object on x86</p>



<a name="133152717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152717">(Aug 31 2018 at 22:40)</a>:</h4>
<p>but that _should not_ come into it</p>



<a name="133152724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152724">(Aug 31 2018 at 22:41)</a>:</h4>
<p>ok good, but then i am <em>really</em> confused about what you're arguing</p>



<a name="133152741"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152741" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152741">(Aug 31 2018 at 22:41)</a>:</h4>
<p>what's important is that, on the virtual machine, you're doing a load of an <code>X</code> value from memory, and that the invariants _must_ be valid</p>



<a name="133152788"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152788" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152788">(Aug 31 2018 at 22:42)</a>:</h4>
<p>wait i thought you were advocating that in this scenario there's only values, nothing involving memory, least of all a load</p>



<a name="133152804"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152804" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152804">(Aug 31 2018 at 22:43)</a>:</h4>
<p>I mean, it depends on what you pass? I was assuming that you were loading from the stack when you're passing, but I guess you could also pass an rvalue expression in which case no loads happen</p>



<a name="133152825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152825">(Aug 31 2018 at 22:43)</a>:</h4>
<p>so that load you refer to would have happened in the caller, if at all?</p>



<a name="133152829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152829">(Aug 31 2018 at 22:44)</a>:</h4>
<p>yep</p>



<a name="133152873"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152873" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152873">(Aug 31 2018 at 22:44)</a>:</h4>
<p>and the reason why <code>foo</code> can assume <code>x.z</code> is non-null is a definition of validity on <code>X</code> <em>values</em>, recursing into the fields?</p>



<a name="133152898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152898">(Aug 31 2018 at 22:45)</a>:</h4>
<p>yes - if you have a value of type <code>T</code>, that value must be valid</p>



<a name="133152903"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133152903" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133152903">(Aug 31 2018 at 22:45)</a>:</h4>
<p>if it's invalid in some way, then you've got UB</p>



<a name="133153059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153059">(Aug 31 2018 at 22:48)</a>:</h4>
<p>ok so for contrast: the <code>nonnull</code> attribute can be justified in an untyped-memory model if you put <code>X</code> in memory and pass it by reference (note: this is different from passing <code>&amp;X</code>!) -- you enforce the validity invariant for <code>X</code> on the memory of the argument on entry</p>



<a name="133153137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153137">(Aug 31 2018 at 22:50)</a>:</h4>
<p>yes, but then you have a weird model where you're enforcing validity invariants "at some points"</p>



<a name="133153147"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153147" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153147">(Aug 31 2018 at 22:50)</a>:</h4>
<p>instead of at exactly one point - any time there's an rvalue conversion</p>



<a name="133153150"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153150" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153150">(Aug 31 2018 at 22:50)</a>:</h4>
<p><code>noalias</code> gets into the stacked borrows proposal but there likewise you can recurse into memory you own (going through <code>&amp;_</code> is unlikely to fly for other reasons), you just have to do it "on memory" rather than having values that represent aggregates</p>



<a name="133153165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153165">(Aug 31 2018 at 22:51)</a>:</h4>
<p>in a model where rvalues are so pervasive, surely operations on them could result in invalid rvalues? when do those trigger UB? (and how do you even represent them in the data model)</p>



<a name="133153254"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153254" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153254">(Aug 31 2018 at 22:54)</a>:</h4>
<p>It makes it really clear why this code (<a href="#narrow/stream/136281-wg-unsafe-code-guidelines/subject/Accessing.20uninitialized.20field.20lvalues/near/133104916" title="#narrow/stream/136281-wg-unsafe-code-guidelines/subject/Accessing.20uninitialized.20field.20lvalues/near/133104916">https://rust-lang.zulipchat.com/#narrow/stream/136281-wg-unsafe-code-guidelines/subject/Accessing.20uninitialized.20field.20lvalues/near/133104916</a>) is valid -</p>
<div class="codehilite"><pre><span></span><span class="kd">let</span><span class="w"> </span><span class="n">ptr</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">alloc</span>::<span class="n">alloc</span><span class="p">(</span><span class="n">layout</span><span class="p">)</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">IdentifierInner</span><span class="p">;</span><span class="w"></span>
<span class="n">std</span>::<span class="n">ptr</span>::<span class="n">write</span><span class="p">(</span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="p">(</span><span class="o">*</span><span class="n">ptr</span><span class="p">).</span><span class="n">size</span><span class="p">,</span><span class="w"> </span><span class="n">size</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="kt">u32</span><span class="p">);</span><span class="w"></span>

<span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">buff</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">std</span>::<span class="n">slice</span>::<span class="n">from_raw_parts_mut</span><span class="p">((</span><span class="o">*</span><span class="n">ptr</span><span class="p">).</span><span class="n">mut_ptr</span><span class="p">(),</span><span class="w"> </span><span class="n">size</span><span class="p">);</span><span class="w"></span>
<span class="k">for</span><span class="w"> </span><span class="n">ch</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="p">.</span><span class="n">nfc</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="kd">let</span><span class="w"> </span><span class="n">offset</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">ch</span><span class="p">.</span><span class="n">encode_utf8</span><span class="p">(</span><span class="n">buff</span><span class="p">).</span><span class="n">len</span><span class="p">();</span><span class="w"></span>
<span class="w">  </span><span class="n">buff</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">buff</span><span class="p">[</span><span class="n">offset</span><span class="p">..];</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>because you never do an rvalue conversion - <code>(*ptr).size</code> is an lvalue expression of type <code>u32</code>, and you immediately give that lvalue expression to an <code>&amp;mut</code> operator, which converts the lvalue T to an rvalue &amp;mut T. There's no read of the <code>T</code></p>



<a name="133153301"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153301" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153301">(Aug 31 2018 at 22:54)</a>:</h4>
<p>similarly with <code>buff[offset...]</code> - the lvalue expression is immediately passed to the <code>&amp;mut</code> operator</p>



<a name="133153374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153374">(Aug 31 2018 at 22:56)</a>:</h4>
<p>"there is no load of the u32 at <code>(*ptr).size</code>" is also true and also relevant in the style of model ralf has developed</p>



<a name="133153391"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153391" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153391">(Aug 31 2018 at 22:57)</a>:</h4>
<p>yes, because you never do an rvalue conversion - that's the literal "thing" that happens in Rust</p>



<a name="133153443"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153443" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153443">(Aug 31 2018 at 22:58)</a>:</h4>
<p>it feels like you're just saying "load" when you mean "rvalue conversion", except we pretend that that load goes directly into memory in between. You could definitely lower Rust into these memory semantics, but it seems odd?</p>



<a name="133153466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153466">(Aug 31 2018 at 22:59)</a>:</h4>
<p>in this example there's no interesting differences between scalars+memory vs values+objects, because everything's happening in terms of scalars (ints and slice references)</p>



<a name="133153514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153514">(Aug 31 2018 at 23:00)</a>:</h4>
<p>and it means, imo, that you now have to do a mental lowering from Rust semantics to low-level memory semantics to figure out whether you're doing something bad, which seems unfortunate, as opposed to just using Rust semantics in the model definition.</p>



<a name="133153560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153560">(Aug 31 2018 at 23:01)</a>:</h4>
<p>ok i see where you are going</p>



<a name="133153569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153569">(Aug 31 2018 at 23:01)</a>:</h4>
<p>also, it's not operations on scalars - they're operations on <code>IdentifierInner</code></p>



<a name="133153576"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153576" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153576">(Aug 31 2018 at 23:01)</a>:</h4>
<p>the lvalue expressions are on an uninitialized <code>IdentifierInner</code>, which is what makes it interesting</p>



<a name="133153632"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153632" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153632">(Aug 31 2018 at 23:03)</a>:</h4>
<p>at least, imo</p>



<a name="133153635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153635">(Aug 31 2018 at 23:03)</a>:</h4>
<p>i can't think of any projections through lvalues that we've ever wanted to consider UB?</p>



<a name="133153694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153694">(Aug 31 2018 at 23:04)</a>:</h4>
<p>as in, expressions like <code>&amp;foo.bar</code> are at most interesting wrt pointer arithmetic and rules about the resulting reference (which may in turn imply a bit about <code>foo</code> though it turns out probably not), not wrt validity of <code>foo</code> in itself</p>



<a name="133153703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153703">(Aug 31 2018 at 23:05)</a>:</h4>
<p>right, exactly - we're projecting through an lvalue, which is distinct from accessing an rvalue? does that make sense?</p>
<p>like, the model in rust is that <code>&amp;foo.bar</code> is an lvalue expression, which is distinct from say, <code>bar(foo)</code> which is an rvalue expression</p>



<a name="133153711"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153711" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153711">(Aug 31 2018 at 23:05)</a>:</h4>
<p>it seems we're in violent agreement here, so moving on</p>



<a name="133153716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153716">(Aug 31 2018 at 23:05)</a>:</h4>
<p>what? you can't disagree, that's literally the model in Rust</p>



<a name="133153717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153717">(Aug 31 2018 at 23:05)</a>:</h4>
<p>that's how the typechecker works</p>



<a name="133153758"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153758" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153758">(Aug 31 2018 at 23:06)</a>:</h4>
<p>hahaha, fair</p>



<a name="133153759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153759">(Aug 31 2018 at 23:06)</a>:</h4>
<p>oops, <em>agreement</em>, not disagreement!!</p>



<a name="133153761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153761">(Aug 31 2018 at 23:06)</a>:</h4>
<p>that's not how this idiom works, brain</p>



<a name="133153769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153769">(Aug 31 2018 at 23:07)</a>:</h4>
<p>so regarding your point about "lowering" rust locations and rvalues to memory accesses - YES that is exactly the point, taking it all much lower level and breaking it down into simpler operations so that the spec is simpler and can be implemented much more directly (as in miri)</p>



<a name="133153776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153776">(Aug 31 2018 at 23:07)</a>:</h4>
<p>this does, as you say, place some burden on people looking at source code</p>



<a name="133153780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153780">(Aug 31 2018 at 23:07)</a>:</h4>
<p>yeah - my interest is making it easier for people who are reading and writing source code, as opposed to those who are writing the spec</p>



<a name="133153822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153822">(Aug 31 2018 at 23:08)</a>:</h4>
<p>it's not just easier on the spec writers, it's also easier on rustc and miri developers</p>



<a name="133153824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153824">(Aug 31 2018 at 23:08)</a>:</h4>
<p>because it's literally how MIR works</p>



<a name="133153830"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153830" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153830">(Aug 31 2018 at 23:08)</a>:</h4>
<p>sure; they're not who I'm interested in making the lives of easier tho :)</p>



<a name="133153852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153852">(Aug 31 2018 at 23:09)</a>:</h4>
<p>ah but a better miri means you often won't have to manually reason your way through whether something is ub!</p>



<a name="133153914"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153914" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153914">(Aug 31 2018 at 23:10)</a>:</h4>
<p>whether something is UB is a runtime property dependent on data</p>



<a name="133153921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153921">(Aug 31 2018 at 23:10)</a>:</h4>
<p>I doubt Miri's ability to solve the halting problem</p>



<a name="133153996"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133153996" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133153996">(Aug 31 2018 at 23:13)</a>:</h4>
<p>very funny. many questions do boil down to a specific litmus test with only one or two relevant traces, though</p>



<a name="133154041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133154041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133154041">(Aug 31 2018 at 23:14)</a>:</h4>
<p>such as your example from above -- the addresses and buffer length don't matter, you just run it once with one input, miri doesn't complain about accessing an unintialized <code>size</code>, and you're in the clear</p>



<a name="133154959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133154959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133154959">(Aug 31 2018 at 23:41)</a>:</h4>
<p>one other thought -- it's not unheard of to have multiple specs in a different style and prove them equivalent (or give a sound mapping from one to another). if a c++ style model is significantly easier to reason about for programmers -- which i am still not really sure about -- it might nevertheless make sense for the UCG to produce a simple low-level spec, implement it in miri, etc. and (later) provide programmers with a c++ style explanation that is proven equivalent</p>
<p>however there is a very real chance that there will be differences (possibly only in edge cases) between the natural way to formulate these two models. in any case we won't know this until someone (<em>cough</em>) sits down and writes out a concrete proposal to compare and contrast</p>



<a name="133155524"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133155524" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133155524">(Aug 31 2018 at 23:59)</a>:</h4>
<p>it's possible <code>nfc</code> has a bug for specific characters, tho</p>



<a name="133155530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133155530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133155530">(Aug 31 2018 at 23:59)</a>:</h4>
<p>or <code>size_utf8</code>, or <code>encode_utf8</code></p>



<a name="133168485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168485">(Sep 01 2018 at 08:05)</a>:</h4>
<blockquote>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> that's not necessarily true - for example, <code>Box&lt;T&gt;</code> should always be non-zero when it's a value</p>
</blockquote>
<p>Fair. Lang items are primitive types.</p>



<a name="133168530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168530">(Sep 01 2018 at 08:06)</a>:</h4>
<p>But this is just a validity invariant</p>



<a name="133168542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168542">(Sep 01 2018 at 08:07)</a>:</h4>
<p>which applies every time you "touch" data -- so again, the type comes from the operation. Doing assignment at type <code>T</code>? Copy the bytes, and enforce that they form a valid <code>T</code>. Everything is still bytes.</p>



<a name="133168603"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168603" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168603">(Sep 01 2018 at 08:09)</a>:</h4>
<p>and I think passing values between functions through memory is a great way to side-step many annoying questions.</p>



<a name="133168666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168666">(Sep 01 2018 at 08:11)</a>:</h4>
<p>arguments, on the caller side, are an <code>Operand</code>, and on the callee side a <code>Place</code>. so the most natural thing to do for argument passing is "copy operand to place", an operation we <em>have to define anyway</em>. This is also what happens in miri, btw.</p>



<a name="133168673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168673">(Sep 01 2018 at 08:11)</a>:</h4>
<p>and every time we write anything to a place, that operation happens at a type. so we copy the bytes, and then enforce validity of them according to said type.</p>



<a name="133168675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168675">(Sep 01 2018 at 08:11)</a>:</h4>
<p>(I plan to implement this in miri when I come back from my vacation)</p>



<a name="133168936"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133168936" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133168936">(Sep 01 2018 at 08:20)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> for the record, I have been trying to avoid lvalue and rvalue and prvalue and the roughly one dozen kinds of <code>*value</code> C++ has, because I find this huge amount of terminology very confusing. And in fact the people defining MIR seem to think the same way. So MIR has places, which roughly correspond to lvalues, and Operands, which roughly correspond to rvalues.</p>
<p><code>(*ptr).size</code> is indeed a place, and then for argument passing there is a <code>_tmp = &amp;mut (*ptr).size</code> where <code>&amp;mut</code> is the operation defining how the place of the left is to be filled; in this case, it is with the location (and metadata) computed on the right. There is actually no <code>Operand</code>/rvalue anywhere in this expression. MIR does not allow nesting <code>&amp;mut</code> in other expressions, so we can avoid that complication. So indeed the data "pointed to" by the <code>Place</code> <code>(*ptr).size</code> is never touched, and does not have to be valid; just the place itself must be valid.</p>
<p>I see no need to introduce compound values here.</p>



<a name="133169038"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133169038" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133169038">(Sep 01 2018 at 08:24)</a>:</h4>
<blockquote>
<p>yeah - my interest is making it easier for people who are reading and writing source code, as opposed to those who are writing the spec</p>
</blockquote>
<p>I think that is a luxury we can try to achieve once we have a spec. First of all, I disagree that a spec with compound values is easier for people who are reading and writing source code, except if you restrict yourself to safe code only where there is hardly ever any disagreement about what the code will do.<br>
However, irrespective of that, given how hard it is to spec low-level languages, we should do everything we can to make the work simpler for the spec writers. Finally, given that the spec is <em>trusted</em> in the sense that any proof about any Rust program ever takes the spec as a given, and relies on the spec making sense, it is of paramount importance to make the spec as easy to read as we possibly can. Basically, everything the spec says should be immediately obviously sensible to anyone reading it, so that w can have as many eyes as possible on it. If we screw up the spec, the entire tower resting on top of it crumbles. the harder to read a spec is, the less useful it is as a foundation for a language.</p>



<a name="133169397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133169397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133169397">(Sep 01 2018 at 08:38)</a>:</h4>
<p>(And with that I am leaving for my vacation, see you in two weeks!)</p>



<a name="133172570"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172570" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172570">(Sep 01 2018 at 10:33)</a>:</h4>
<blockquote>
<p>for example in <code>let PAT = EXPR;</code> evaluation of <code>EXPR</code> writes the result to a temporary memory locations, and the <code>let</code> copies parts of that into named (and possibly longer-lived) memory locations</p>
</blockquote>
<p>I just want to point that this is exactly how it is desugared in MIR. For a non-trivial pattern, we first store EXPR into a temporary and then "move" that temporary into <code>PAT</code>. For a trivial pattern like <code>x</code>, we store directly into the memory for <code>x</code>.</p>



<a name="133172658"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172658" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172658">(Sep 01 2018 at 10:35)</a>:</h4>
<p>that last part is quite important though, and my not mentioning it has caused confusion, mea culpa</p>



<a name="133172779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172779">(Sep 01 2018 at 10:38)</a>:</h4>
<blockquote>
<p>that last part is quite important though, and my not mentioning it has caused confusion, mea culpa</p>
</blockquote>
<p>it's just an optimization, though</p>



<a name="133172781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172781">(Sep 01 2018 at 10:38)</a>:</h4>
<p>we just wanted to avoid a temporary</p>



<a name="133172784"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172784" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172784">(Sep 01 2018 at 10:39)</a>:</h4>
<p>I don't think it's significant in any other way?</p>



<a name="133172831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthew Jasper <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172831">(Sep 01 2018 at 10:40)</a>:</h4>
<p>It's visible in cases like <a href="https://github.com/rust-lang/rust/issues/53695" target="_blank" title="https://github.com/rust-lang/rust/issues/53695">#53695</a></p>



<a name="133172843"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172843" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172843">(Sep 01 2018 at 10:40)</a>:</h4>
<blockquote>
<p>yeah - my interest is making it easier for people who are reading and writing source code, as opposed to those who are writing the spec</p>
</blockquote>
<p>ps, <span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span>, I strongly agree with this ambition! However, I am not sure what is the best way to achieve it.</p>
<p>In particular, I think that it often happens that unsafe code authors start with a view of what they want the hardware to do, and then work <strong>up</strong> to how to express that in Rust. In this case, having the spec be expressed in terms of more low-level concepts is helpful.</p>



<a name="133172852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172852">(Sep 01 2018 at 10:41)</a>:</h4>
<blockquote>
<p>It's visible in cases like <a href="https://github.com/rust-lang/rust/issues/53695" target="_blank" title="https://github.com/rust-lang/rust/issues/53695">#53695</a></p>
</blockquote>
<p>hmm, I suppose that's true.</p>



<a name="133172853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172853">(Sep 01 2018 at 10:41)</a>:</h4>
<p>well, that depends</p>



<a name="133172896"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172896" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172896">(Sep 01 2018 at 10:42)</a>:</h4>
<p>but yeah it depends on when the "pattern storing" takes place, and I guess that most logically it would take place after the block's data has been dropped</p>



<a name="133172899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172899">(Sep 01 2018 at 10:42)</a>:</h4>
<p>i meant it caused confusion about the mental model, or how we justify validating the scalar corresponding to <code>Box&lt;_&gt;</code> (that was the context in which i wrote that)</p>



<a name="133172900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172900">(Sep 01 2018 at 10:42)</a>:</h4>
<p>that's an interesting point <span class="user-mention" data-user-id="116118">@Matthew Jasper</span> that perhaps affects my opinion about that issue :)</p>



<a name="133172903"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172903" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172903">(Sep 01 2018 at 10:43)</a>:</h4>
<blockquote>
<p>i meant it caused confusion about the mental model, or how we justify validating the scalar corresponding to <code>Box&lt;_&gt;</code> (that was the context in which i wrote that)</p>
</blockquote>
<p>I don't see why</p>



<a name="133172906"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172906" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172906">(Sep 01 2018 at 10:43)</a>:</h4>
<p>in particular, in both cases, we are storing into memory?</p>



<a name="133172909"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172909" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172909">(Sep 01 2018 at 10:43)</a>:</h4>
<p>in one case, we store directly to the memory for the local varibale, in the other to a temporary?</p>



<a name="133172911"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172911" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172911">(Sep 01 2018 at 10:43)</a>:</h4>
<p>I guess I have to re-read that part of your discussion, I got a bit lost there</p>



<a name="133172912"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172912" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172912">(Sep 01 2018 at 10:43)</a>:</h4>
<p>anyway, I should go do weekend things too <span class="emoji emoji-1f3d6" title="beach">:beach:</span> :P</p>



<a name="133172960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133172960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133172960">(Sep 01 2018 at 10:44)</a>:</h4>
<p>hm yes, the core thing i missed was that we can and should validate scalars when storing, not just when loading</p>



<a name="133173033"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173033" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173033">(Sep 01 2018 at 10:46)</a>:</h4>
<p>i was very incorrectly going with "scalars are validated on loads" and then the extra copy is significant</p>



<a name="133173046"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173046" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173046">(Sep 01 2018 at 10:47)</a>:</h4>
<p>ah, I see, yes, that makes sense :)</p>



<a name="133173096"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173096" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173096">(Sep 01 2018 at 10:48)</a>:</h4>
<p>well, I may also be mistaken, it's worth keeping in mind, particularly seeing as MIR does this optimization</p>



<a name="133173102"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173102" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173102">(Sep 01 2018 at 10:49)</a>:</h4>
<p>(and I believe that our first efforts at defining UB semantics will probably begin from MIR)</p>



<a name="133173106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173106">(Sep 01 2018 at 10:49)</a>:</h4>
<p>though it of course means we have to define lowering into MIR to get a full round-trip</p>



<a name="133173109"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173109" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173109">(Sep 01 2018 at 10:49)</a>:</h4>
<p>but then we sort of need that anyway, because otherwise we can't really spec out the borrow checker</p>



<a name="133173162"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173162" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173162">(Sep 01 2018 at 10:50)</a>:</h4>
<p>i think it makes sense to define all evaluation wrt to a destination location, and then speccing this behavior is just a matter of passing along the right destination location in various contexts</p>



<a name="133173289"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173289" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173289">(Sep 01 2018 at 10:55)</a>:</h4>
<p>it makes sense to look at MIR construction here — we have a few different "modes" of evaluation ultimately</p>



<a name="133173290"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173290" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173290">(Sep 01 2018 at 10:55)</a>:</h4>
<p>but maybe those can be viewed as optimizations</p>



<a name="133173332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173332">(Sep 01 2018 at 10:56)</a>:</h4>
<p>(and we'd want to show then that they are valid)</p>



<a name="133173333"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173333" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173333">(Sep 01 2018 at 10:56)</a>:</h4>
<p>e.g., we don't make a temporary value for something like <code>foo(22)</code> =)</p>



<a name="133173342"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173342" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173342">(Sep 01 2018 at 10:57)</a>:</h4>
<p>still, it'd obviously be nice to keep the "reference model" as simple as possible</p>



<a name="133173346"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173346" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173346">(Sep 01 2018 at 10:57)</a>:</h4>
<p>(and — in the early days of MIR — we did make temporaries for all those cases...)</p>



<a name="133173348"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173348" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173348">(Sep 01 2018 at 10:57)</a>:</h4>
<blockquote>
<p>it makes sense to look at MIR construction here — we have a few different "modes" of evaluation ultimately</p>
</blockquote>
<p>this is a very good point, i am actually tragically uninformed about mir construction</p>



<a name="133173350"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173350" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173350">(Sep 01 2018 at 10:57)</a>:</h4>
<p>the main other one is evaluating to a "place"</p>



<a name="133173354"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173354" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173354">(Sep 01 2018 at 10:57)</a>:</h4>
<p>e.g. for things like <code>&amp;foo.bar</code></p>



<a name="133173356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173356">(Sep 01 2018 at 10:57)</a>:</h4>
<p>in cases like <code>&amp;bar()</code> it creates a temporary and returns that</p>



<a name="133173399"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173399" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173399">(Sep 01 2018 at 10:58)</a>:</h4>
<p>ah but this is 1. crucial for the semantics and 2. based on a syntactic classification of place expressions vs value expressions, right?</p>



<a name="133173400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173400">(Sep 01 2018 at 10:58)</a>:</h4>
<p>yes</p>



<a name="133173402"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173402" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173402">(Sep 01 2018 at 10:58)</a>:</h4>
<p>I raised it because it is a distinction we cannot eliminate</p>



<a name="133173411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133173411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133173411">(Sep 01 2018 at 10:59)</a>:</h4>
<p>ok enough of my edification, go do weekend things :)</p>



<a name="133178370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133178370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133178370">(Sep 01 2018 at 13:47)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I absolutely disagree, I guess, on how people write unsafe code. as a C++ developer with access to a good standard, I do not go that way at all; I look at how to solve my problems in the abstract model of C++.</p>



<a name="133178412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133178412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133178412">(Sep 01 2018 at 13:48)</a>:</h4>
<p>similar to most other people I know in the C++ community</p>



<a name="133178487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133178487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133178487">(Sep 01 2018 at 13:50)</a>:</h4>
<p>and I want Rust to be that way. I don't want people to think "oh, I want to have a tagged pointer, I should give myself a pointer type and then tag the bottom bits, because that is valid on the hardware". I want someone to think "oh, I should have a <code>usize</code> which can be cast to a pointer, because rvalue-conversion on an invalid pointer is suspect at best"</p>



<a name="133178835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133178835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133178835">(Sep 01 2018 at 14:00)</a>:</h4>
<blockquote>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> for the record, I have been trying to avoid lvalue and rvalue and prvalue and the roughly one dozen kinds of <code>*value</code> C++ has, because I find this huge amount of terminology very confusing. And in fact the people defining MIR seem to think the same way. So MIR has places, which roughly correspond to lvalues, and Operands, which roughly correspond to rvalues.</p>
<p><code>(*ptr).size</code> is indeed a place, and then for argument passing there is a <code>_tmp = &amp;mut (*ptr).size</code> where <code>&amp;mut</code> is the operation defining how the place of the left is to be filled; in this case, it is with the location (and metadata) computed on the right. There is actually no <code>Operand</code>/rvalue anywhere in this expression. MIR does not allow nesting <code>&amp;mut</code> in other expressions, so we can avoid that complication. So indeed the data "pointed to" by the <code>Place</code> <code>(*ptr).size</code> is never touched, and does not have to be valid; just the place itself must be valid.</p>
<p>I see no need to introduce compound values here.</p>
</blockquote>
<p>It's really not that hard, and it's kind of necessary to understand for purposes of typechecking Rust. There are 3 kinds of values in C++, and two categories, but one of those value kinds is unnecessary in Rust, and so the categories don't need to exist either.</p>
<p>There are two kinds of things, lvalues, and rvalues. An lvalue is any expression which refers to a specific place in memory, and you can only access one of these through the <code>*</code> or <code>[]</code> operators. An rvalue is any expression which is not an lvalue. An rvalue conversion is when you want an rvalue (for example, to initialize a stack-local) but all you have is an lvalue.</p>
<p>(note: There are three kinds of lvalues - read, read-write, and owned.)</p>
<p>This is why I say it's not that complicated, and also, you need to understand this stuff anyways if you want to understand some stuff that Rust does around Drop/non-Copy types, and lifetimes, so I think it's entirely valid to define a model in terms of these things that Rust programmers should inherently understand. We should not define the model in terms of MIR, a specific lowering of Rust _that changes_ depending on optimizations and versions of Rust. I want to know what a valid lowering of Rust to assembler is, which means we should define a model in terms of Rust.</p>



<a name="133412029"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133412029" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133412029">(Sep 06 2018 at 00:14)</a>:</h4>
<p>I will admit, I have skimmed a lot of this conversation. I'm starting to think that the ideal model is to try to think of a value-level semantics in a way that becomes easy to translate things upward.</p>
<blockquote>
<p>whether something is UB is a runtime property dependent on data</p>
</blockquote>
<p>This stood out to me, in part because it's true, but in particular because I feel like we generally do not want UB to be dependent on the compiler. It ought not be possible to argue that a given interaction is fine simply because the compiler lets it happen sometimes. Any purely hardware-based or representation-based semantics would allow that, I think.</p>
<p>A purely object-value based semantics like C's and C++'s are also difficult, however, because they lead to a lot of confusion and disagreement and underspecifiedness.</p>



<a name="133412720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133412720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133412720">(Sep 06 2018 at 00:27)</a>:</h4>
<p>So perhaps there's some middle ground where we could define a machine which is concrete enough to code and teach people by, but abstract enough not to let coincidences slip by? I guess my metric here would be "could we theoretically write a run-time sanitizer for this".</p>



<a name="133412879"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133412879" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133412879">(Sep 06 2018 at 00:30)</a>:</h4>
<p>(I suspect the answer is that yes, we could do so, provided that the program doesn't move bytes outside the sanitizer's purview. But we could imagine a world where e.g. the VM's extra tagging could include the filesystem and networked applications and such. I think the same would apply to RalfJ's tags in the stacked borrowed model)</p>



<a name="133424265"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133424265" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133424265">(Sep 06 2018 at 06:17)</a>:</h4>
<p>I had a nice conversation tonight with <span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> on Discord and I think I'm pretty much in agreement with her. The stuff I wrote above seems wrong at the edges, so please don't nitpick it too deeply. ;)</p>



<a name="133424315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133424315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133424315">(Sep 06 2018 at 06:19)</a>:</h4>
<p>Although I just mean that about the stuff I wrote above. I'm unsure about lvalue/rvalue terminology, except to say that if we agree on the concepts then I'm not too concerned for now about the actual terms for them.</p>



<a name="133432362"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133432362" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133432362">(Sep 06 2018 at 09:52)</a>:</h4>
<p><span class="user-mention" data-user-id="123893">@alercah</span> link to conversation, perhaps?</p>



<a name="133456206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133456206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133456206">(Sep 06 2018 at 17:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> it was in a private message</p>



<a name="133581798"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/133581798" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> alercah <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#133581798">(Sep 08 2018 at 21:04)</a>:</h4>
<p>(oh, nvm, already addressed)</p>



<a name="134117058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117058">(Sep 17 2018 at 18:07)</a>:</h4>
<p><span class="user-mention" data-user-id="125253">@Nicole Mazzuca</span> </p>
<blockquote>
<p>This is why I say it's not that complicated, and also, you need to understand this stuff anyways if you want to understand some stuff that Rust does around Drop/non-Copy types, and lifetimes, so I think it's entirely valid to define a model in terms of these things that Rust programmers should inherently understand. We should not define the model in terms of MIR, a specific lowering of Rust _that changes_ depending on optimizations and versions of Rust. I want to know what a valid lowering of Rust to assembler is, which means we should define a model in terms of Rust.</p>
</blockquote>
<p>Rust is way too high-level to be specified directly. Things like pattern matching, struct initializers and other complex compound expressions should be desugared to a core language. I think it is one of the big mistakes of C/C++ to not do this. For the same reason that compiling C, C++ or Rust directly to hardware is hard and full of redundancy, it is not a good idea to specify them directly. IRs are extremely useful as a specification device, not just as building block of a compiler. For example, the fact that miri can "specify" (implement, really) Rust behavior without any notion of "read, read/write and owned" values to me is a big sign saying that we do not actually need these notions to talk about Rust behavior.</p>
<p>That core language does not have to be MIR, but I think something close to MIR is a pretty good choice.</p>



<a name="134117197"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117197" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117197">(Sep 17 2018 at 18:10)</a>:</h4>
<blockquote>
<p>An lvalue is any expression which refers to a specific place in memory, and you can only access one of these through the * or [] operators. An rvalue is any expression which is not an lvalue. </p>
</blockquote>
<p>Your notion of a "value" must be very far from mine. In my world (using the usual PL terminology), expressions <em>evaluate to values</em>, but most of the time they <em>are not</em> values. A value is a fully computed "thing" -- a number, or a memory location, or so. It is something static. An expression is a computation that results in a value, it is something dynamic (and then we can bikeshed about whether it can have sideffects or whether those are treated separately).</p>



<a name="134117836"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117836" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117836">(Sep 17 2018 at 18:20)</a>:</h4>
<p>the key thing is that an "lvalue" is really not a value, but an expression</p>



<a name="134117850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117850">(Sep 17 2018 at 18:20)</a>:</h4>
<p>basically synonym for a MIR <code>Place</code></p>



<a name="134117881"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117881" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117881">(Sep 17 2018 at 18:21)</a>:</h4>
<p>or at least that's how I think of it...</p>



<a name="134117892"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134117892" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134117892">(Sep 17 2018 at 18:21)</a>:</h4>
<p>...I am not sure perhaps the C++ Spec has a distinct notion</p>



<a name="134118023"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134118023" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134118023">(Sep 17 2018 at 18:23)</a>:</h4>
<p>an lvalue or place is not a source language expression, although it includes field accesses and indexing and so on just as source language expressions do, so it's confusing to call it "expression" IMO. i prefer to think of them as something analogous to values, though with more complicated structure than e.g. u32</p>



<a name="134121060"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134121060" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134121060">(Sep 17 2018 at 19:15)</a>:</h4>
<p>As a compiler user not author, I've always found the terms "lvalue" and "rvalue" extremely opaque and generally not useful. I don't know how much y'all want to try to stick to existing / established terms vs making it more accessible tho.</p>



<a name="134121141"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134121141" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134121141">(Sep 17 2018 at 19:16)</a>:</h4>
<p>you're right, they're crap terms. we've already moved to "place" instead of "lvalue" in compiler internal identifiers and the reference, and i think i'm not the only one who would prefer to follow up by calling "rvalues" simply "values"</p>



<a name="134124055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134124055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134124055">(Sep 17 2018 at 20:16)</a>:</h4>
<p>Still candidates for the hypothetical glossary I advocate for ;-)</p>



<a name="134130079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134130079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> avadacatavra <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134130079">(Sep 17 2018 at 22:12)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span> the glossary isn't hypothetical! it's just...not totally filled out (but i stuck it in the mdbook because i want it too!)</p>



<a name="134130106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134130106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134130106">(Sep 17 2018 at 22:12)</a>:</h4>
<p>oh, neat... where might I find it?</p>



<a name="134130115"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134130115" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134130115">(Sep 17 2018 at 22:12)</a>:</h4>
<p>s/hypothetical/unknown to me/</p>



<a name="134140642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134140642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134140642">(Sep 18 2018 at 02:18)</a>:</h4>
<p><span class="user-mention" data-user-id="124289">@rkruppe</span> they are definitely non-descriptive, and value/place are better terms.</p>



<a name="134140667"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134140667" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicole Mazzuca <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134140667">(Sep 18 2018 at 02:19)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> I just fundamentally disagree. You can write your models all you want, but what's useful to the average rust programmer is a model in terms of Rust, not a model in terms of an IR that is definitely not Rust.</p>



<a name="134150522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134150522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134150522">(Sep 18 2018 at 07:32)</a>:</h4>
<p><span class="user-mention" data-user-id="124289">@rkruppe</span> </p>
<blockquote>
<p>i think i'm not the only one who would prefer to follow up by calling "rvalues" simply "values"</p>
</blockquote>
<p>MIR/miri call them "operands". Personally I find "value" a bit confusing there because operands can live in memory (in <code>x = y;</code>, when <code>y</code> is big, what is the value? we do a memcpy here, not a "first load, then store".<br>
However, it is possible that this is just an optimization -- that we can see values as "chunks of bytes", and the fact that an operand "delays" the load is not actually observable. that would be a nice model indeed, I think, and then we can call them "values".</p>



<a name="134150546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134150546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134150546">(Sep 18 2018 at 07:33)</a>:</h4>
<p>On the subject of places, I think the "value" content here is a memory address. that is more complicated than <code>u32</code> indeed, but not very much so. In miri, a place is a triple of a pointer, an expected alignment, and metadata for unsized places.</p>



<a name="134150607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134150607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134150607">(Sep 18 2018 at 07:34)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span> seems the glossary is at <a href="https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md" target="_blank" title="https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md">https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md</a>. Took me a bit to find it because the filename does not exactly give it away^^</p>



<a name="134151147"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134151147" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134151147">(Sep 18 2018 at 07:49)</a>:</h4>
<blockquote>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> I just fundamentally disagree. You can write your models all you want, but what's useful to the average rust programmer is a model in terms of Rust, not a model in terms of an IR that is definitely not Rust.</p>
</blockquote>
<p>What I am arguing for is that the best and most useful way to describe a complicated thing is by describing it in terms of something simpler. Instead of doing one HUGE step -- a direct semantics for surface-level Rust -- we do two much smaller steps: A semantics for a language with few, easy to understand concepts; and a translation into that language. the translation takes care of concerns like evaluation order and other things I mentioned. I think this is much more useful to a programmer than a complex HUGE direct semantics, because there is actually a chance they might understand it. Sometimes, adding an intermediate abstraction provides an overall huge complexity <em>reduction</em> and thus makes things much easier to understand, and I strongly believe language semantics is one of these cases. A direct semantics for the surface language is near useless as it is too complex, not understandable.</p>
<p>I see a bunch of evidence for this:</p>
<ul>
<li>C/C++ are baroque standards, where even experts can argue for days about corner cases. It's not just me who thinks an abstract machine with a simpler language would make a big difference here, see also e.g. <a href="https://lkml.org/lkml/2018/6/7/761" target="_blank" title="https://lkml.org/lkml/2018/6/7/761">https://lkml.org/lkml/2018/6/7/761</a>.</li>
<li>Compilers introduce IR (several IRs, usually). E.g., Rust got MIR because it was just really hard and error-prone to work with HIR as there are so many powerful language constructs there (and HIR already desugared some stuff, but not enough). Surface languages are not even suited for compiler authors to think about program behavior, that makes them even less suited to programmers less famililar with the language.</li>
<li>The vast majority of formal research on real languages proceeds by extracting a core calculus, again because there is a huge amount of complexity reduction achieved when one can first translate individual complex statements to sequences of simple statements, and then describe how the individual simple statements work.</li>
<li>There is precedence for this in a light form even for PL standards, e.g. JavaScript describes the <a href="https://www.ecma-international.org/ecma-262/8.0/index.html#sec-if-statement" target="_blank" title="https://www.ecma-international.org/ecma-262/8.0/index.html#sec-if-statement">semantics of every statement</a> etc. as a sequence of simple operations. These simple operations are in plain English, not in a proper formal language, but they are close enough that work on formalizing JS was able to turn the simple operations into a core language, translate the standard line-by-line into Coq, and obtain a proper formal semantics of JS that agrees very well with real implementations. See <a href="https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2018JaVerT.html" target="_blank" title="https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2018JaVerT.html">https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2018JaVerT.html</a>.</li>
<li>This doesnt just apply to programming languages; the official ARM documentation works the same way: Every instruction (many of which have multiple effects, e.g. multiple memory accesses etc.) is explained by a sequence of even-lower-level instructions that do one thing and one thing only. See <a href="https://static.docs.arm.com/ddi0557/ab/DDI0557A_b_armv8_1_supplement.pdf" target="_blank" title="https://static.docs.arm.com/ddi0557/ab/DDI0557A_b_armv8_1_supplement.pdf">https://static.docs.arm.com/ddi0557/ab/DDI0557A_b_armv8_1_supplement.pdf</a> and <a href="https://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf" target="_blank" title="https://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf">https://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf</a>.</li>
</ul>



<a name="134178549"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134178549" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134178549">(Sep 18 2018 at 16:57)</a>:</h4>
<p>So, I'd like to step back. I have a feeling that we all share the same endgoals:</p>
<ul>
<li>We want a spec that can serve <em>users</em> and <em>compiler authors</em></li>
<li>We want a spec that is clear and — to the extent possible — checkable in an automated fashion</li>
</ul>
<p>My belief is that the best route to get there is to operate in layers. That is, defining UB for a "MIR-like" abstraction is hard enough. Assuming we find a model we are happy with, then we can define a mapping from Rust down to MIR, and we have a specification. Perhaps one that is not in the best form for universal consumption, but an actionable one. (And I tend to think that, while most Rust programmers aren't familiar with MIR per se, they have some kind of internal desugaring going on in their heads anyway — e.g., they eventually learn that <code>foo.bar()</code> is sugar for <code>Foo::bar(&amp;foo)</code> and so forth.)</p>
<p>Now, given a specification, the task becomes to <em>explain</em> that spec in various ways such that it is understandable. I imagine that the best way to explain it will depend on the audience. e.g., C programmers might already have a kind of concrete abstraction for the machine and would prefer to start from a MIR-like level. People coming to Rust from some other background might prefer a different approach. </p>
<p>In terms of audiences, I do think that compiler authors hold a mildly privileged space, in that (as <span class="user-mention" data-user-id="120791">@RalfJ</span> pointed out), they are the ones who have to apply the spec to decide whether a given optimization fits and so forth, as well as implementing dynamic checkers. For this reason, I think that having the "primary, normative" variant be done in terms of something quite close to the IR that they will be using for this (MIR) makes sense.</p>



<a name="134178845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134178845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134178845">(Sep 18 2018 at 17:03)</a>:</h4>
<p>I'd expect "revelations" at one layer to propagate up and down the abstraction stack, informing decisions</p>



<a name="134178926"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134178926" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134178926">(Sep 18 2018 at 17:04)</a>:</h4>
<p>I do think it's reasonable to hold off on declaring anything "stable" or "done" until we're confident it can be reasoned about from multiple "angles"</p>



<a name="134178957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134178957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134178957">(Sep 18 2018 at 17:05)</a>:</h4>
<p>and also I should say that when I say "MIR" I don't literally mean the compiler's representation, necessarily, but perhaps a slightly cleaned up and idealized form of it...</p>



<a name="134225029"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134225029" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> avadacatavra <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134225029">(Sep 19 2018 at 11:04)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span> <a href="https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md" target="_blank" title="https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md">https://github.com/rust-rfcs/unsafe-code-guidelines/blob/master/reference/src/introduction.md</a><br>
i stuck it in the intro for now (thinking, maybe we should define terms before using them) but that's mostly just so that we have <em>something</em></p>



<a name="134231199"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants/near/134231199" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/data-invariants.html#134231199">(Sep 19 2018 at 13:14)</a>:</h4>
<p><span class="user-mention" data-user-id="126854">@avadacatavra</span> yup thanks! (<span class="user-mention" data-user-id="120791">@RalfJ</span> linked it earlier and I <a href="https://github.com/rust-rfcs/unsafe-code-guidelines/pull/30" target="_blank" title="https://github.com/rust-rfcs/unsafe-code-guidelines/pull/30">submitted a PR</a> to add some words I'd like defined)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>